{-# LANGUAGE QuasiQuotes, ScopedTypeVariables, TypeOperators, GADTs,
  MultiParamTypeClasses, FlexibleContexts, TypeSynonymInstances,
  FlexibleInstances, UndecidableInstances, TypeFamilies, TemplateHaskell #-}

{- |

Module      :  Data.Yoko.Reduce
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

A @t@-algebra reduces a disbanded @t@ into a mediation of @t@.

-}
module Data.Yoko.Reduce
  (Alg, Algebra(..), AlgebraU(..),
   algebraFin, AlgebraDT(..), AlgebraFin, AlgebraDC(..)) where

import Type.Yoko

import Data.Yoko.Generic
import Data.Yoko.Reflect





-- | A @t@-algebra reduces a disbanded @t@ to the same mediation of @t@.
type Alg m t = Disbanded m t -> Med m t
newtype Algebra m t = Alg (Alg m t); wraps_thinly ''Algebra





-- | @algebraDT@ determines the algebra from the type and mediator.
class DT t => AlgebraDT m t where algebraDT :: Disbanded m t -> Med m t





-- | @algebraUni@ determines the \"algebra\" from the type-sum and mediator.
class AlgebraFin m dcs where
  algebraUni :: AnRMN m dcs -> Med m (LeftmostRange dcs)

data AlgebraU m t where AlgebraU :: (DT t, AlgebraDT m t) => AlgebraU m t
obvious_membership ''AlgebraU

algebraFin :: (AlgebraFin m (Fin u), Finite u) =>
              AnRMN m u -> Med m (LeftmostRange (Fin u))
algebraFin = algebraUni . finiteNP



instance (Med m (LeftmostRange u) ~ Med m (LeftmostRange v),
          AlgebraFin m u, AlgebraFin m v) => AlgebraFin m (u :|| v) where
  algebraUni = algebraUni `two` algebraUni
instance AlgebraDC m dc => AlgebraFin m ((:=:) dc) where
  algebraUni (NP Refl x) = algebraDC x

-- | @algebraDC@ determines the \"alegbra\" from the constructor type and
-- mediator.
class DC dc => AlgebraDC m dc where algebraDC :: RMN m dc -> Med m (Range dc)



two :: (NP u f -> a) -> (NP v f -> a) -> (NP (u :|| v) f -> a)
two f g (NP tag x) = case tag of
  LeftU u -> f $ NP u x
  RightU v -> g $ NP v x
